Nuprl Lemma : non-void-decl-single
11,40
postcript
pdf
T
,
A
:Type,
x
:
T
,
eq
:EqDecider(
T
).
A
non-void(
x
:
A
)
latex
Definitions
t
T
,
P
Q
,
P
Q
,
P
&
Q
,
P
Q
,
x
:
A
.
B
(
x
)
,
x
,
y
.
t
(
x
;
y
)
,
EqDecider(
T
)
,
x
:
v
,
x
dom(
f
).
v
=
f
(
x
)
P
(
x
;
v
)
,
non-void(
d
)
Lemmas
deq
wf
,
fpf-all-single-decl
origin
T, A:Type, x:T, eq:EqDecider(T). A 
non-void(x : A) T, A:Type, x:T, eq:EqDecider(T). A non-void(x : A) 
T Q
Q Qx:A. B(x)
x,y. t(x;y)xdom(f). v=f(x) P(x;v)